;;;; Created on 2012-11-21 21:41:14

(load "p3.lisp")


(defun part_a (sentence)
  (dolist (i sentence)
  ;(write-line (format nil "(part_a ~A ~A)" sentence (wfp-checker sentence)))
  (write-line (format nil "(part_a ~A ~A)" i (wfp-checker i)))
  ))

(defun part_b (sentence interpretation)
  (write-line (format nil "interpretation ~A" interpretation ))
  (write-line (format nil "-----------------------------------"))
  (dolist (i sentence)
  ;(write-line (format nil "sentence: ~A" i ))
  ;(write-line (format nil "============================"))
  (write-line (format nil "(part_b ~A ~A)" i (TruthValue  i interpretation)))
    ))

(defun part_b_tautology (sentence)
  (dolist (i sentence)
  ;(write-line (format nil "(part_a ~A ~A)" sentence (wfp-checker sentence)))
  ;(write-line (format nil "(part_b ~A ~A)" i (TruthValue  i)))
  (write-line (format nil "(part_b ~A ~A)" i (IsTautology i)))
  ))

(defun part_c (sentence)
  (dolist (i sentence)
  ;(write-line (format nil "(part_c ~A ~A)" sentence (wfp-checker sentence)))
  (write-line (format nil "(part_c ~A ~A)" i (wfp-checkerFOL i)))
  ))

;====================================================================
; PART a - Truth Value


(part_a '((f f f) (john is up) p (p q) (AND (OR P (NOT Q)) (OR (NOT P) Q)) (NOT P) (IMPLIES P (Q)) (IMPLIES (P) Q) (EQUIV (P) Q) (EQUIV P (Q)) (|p|)))
(part_a '((P124) ("John is up") (NOT (P)) (AND (P)(Q)) (OR (P)(Q)) (IMPLIES (P)(Q)) (EQUIV (P)(Q)) (EQUIV (IMPLIES (P) (AND (P)(Q))) (NOT (OR (P) (IMPLIES (P)(Q))))) (|p|) (8up) (|not| (P)) (AND (|p|)(Q)) ((P) OR (Q))))
(part_a '((P) (|P|) ("John is up") (NOT (P)) (IMPLIES (P) (Q)) (EQUIV (P) (Q)) (AND (OR (P) (NOT (Q))) (OR (NOT (P)) (Q)))))



;====================================================================
; PART B1 - Truth Value
(setf sentence '((NOT (P))))
(setf sentence '((AND (P)(Q))))
(setf sentence '(((AND) (P)(Q)) (OR (P)(Q))))
(setf sentence '((NOT (P)) (AND (P)(Q)) (OR (P)(Q)) (IMPLIES (P)(Q)) (EQUIV (P)(Q)) 
(EQUIV (IMPLIES (P1) (AND (P2) (Q3))) (NOT (OR (P4) (IMPLIES (P5)(Q6)))))
(IMPLIES (P)(P)) (EQUIV (IMPLIES (P)(Q)) (OR (NOT (P))(Q))) (EQUIV (NOT   
(AND (P)(Q))) (OR (NOT (P))(NOT (Q)))) (IMPLIES (P) (IMPLIES (Q)(P))) (OR
(P) (NOT (P)))))

(setf interpretation '((P t) (Q t) (P1 t) (P2 nil) (Q3 t) (P4 nil) (P5 t) (Q6 nil)))
(setf interpretation '((P nil) (Q nil) (P1 t) (P2 nil) (Q3 t) (P4 nil) (P5 t) (Q6 nil)))

(part_b sentence interpretation)

;====================================================================
; PART B2 -- IsTautology



(setf sentence '((NOT (P)) (AND (P)(Q)) (OR (P)(Q)) (IMPLIES (P)(Q)) (EQUIV (P)(Q)) 
(EQUIV (IMPLIES (P1) (AND (P2) (Q3))) (NOT (OR (P4) (IMPLIES (P5)(Q6)))))
(IMPLIES (P)(P)) (EQUIV (IMPLIES (P)(Q)) (OR (NOT (P))(Q))) (EQUIV (NOT   
(AND (P)(Q))) (OR (NOT (P))(NOT (Q)))) (IMPLIES (P) (IMPLIES (Q)(P))) (OR
(P) (NOT (P)))))

(part_b_tautology sentence)

;====================================================================================================
; PART C -- wfp-checkerFOL

(part_c '((NOT (P |x| |y| |z|)) (P (|f| |b| |y|) |y|) 
          (IMPLIES (Q |u| (|f| |a| |v|) |d|) (R (|g| (|h| |b| |c| |w|)) |y|)) 
          (ALL |x| (IMPLIES (A |x| |c|) (B |x| |d|))) 
          (ALL |x| (EXISTS |y| (IMPLIES (A |y|) (B |x|)))) 
          (AND (ALL |x| (P |x|)) (Q |y| |z|)) 
          (EQUIV (B |f| |u| |a|) (P ())) (P |x| |a| Q)
          (ALL |x| |y| (P |x| |y|)) (ALL |x| (IMPLIES (A |y| |c|) (B |x| |d|))) 
          (ALL |z| (EXISTS |y| (IMPLIES (A |y|) (B |x|))))))




(defun partc-tests ()
  "Unit Tests for part_C"
  
;Should Pass
(part_c '((P)))
(part_c '((P |a|)))
(part_c '((P |x|)))
(part_c '((P |a| |b|)))
(part_c '((AND (I |x|) (P |y|))))
  
(part_c '((P |a| |b| |c|)))
(part_c '((P (|f| |a|))))
(part_c '((P (|f| |a| |b|))))
(part_c '((P (|a| |b|))))
(part_c '((P (|f| |a|))))
(part_c '((NOT (P |x|))))
(part_c '((NOT (P |x| |y| |z|))))
(part_c '((NOT (P |a| |b| |z|))))
(part_c '((OR (P |x| |y| |z|))))
(part_c '((OR(P |a| ) (Q |b| ))))
(part_c '((OR (P))))
(part_c '((IMPLIES (P |a| ) (Q |b| ))))
(part_c '((EQUIV (P |a| ) (Q |b| ))))
(part_c '((ALL |v| (P |v|(|f| |v|)))))
(part_c '((ALL |x| |y| (P |x| |y|))))
(part_c '((EXISTS |v| ( P |v|(|f| |v|)))))

(part_c '("MoveBoat" |x|))


(part_c '((IMPLIES (Q |u| (|f| |a| |v|) |d|) (R (|g| (|h| |b| |c| |w|)) |y|))))


;Should Fail
(part_c '((P |f|)))
(part_c '((P |a| |f|)))
(part_c '((P (|a| |f|))))
(part_c '((EXISTS |v| (P |v| (|v| |f|)))))
  
  
figureout: 

(part_c '((IMPLIES (NOT (OR (P |a|) (Q |b|)))  Q |c|)))

  

  
(setf sent '((ALL |x| |y| (P |x| |y|))))
(handle-quantifiers sent)
(handle-quantifiers '(ALL x y P))
    
(is-alltermsp "ab")
(is-alltermsp '(|a| |b|))
(is-alltermsp '(|a| |z|))
(is-alltermsp '(|a| |f|))
  
  
(term-type "a")
(term-type "f")
(term-type "v")
(term-type "A")
 
(termp "a")
(termp "f")
(termp "v")
(termp "P")
(predicatep "a")
(predicatep "f")
(predicatep "v")
(predicatep "P")
(funcp "a")
(funcp "f")
(funcp "v")
(funcp "P")
  
  )

;====================================================================================================

(defun load-operators (sentence )
  (dolist (i sentence)
  ;(write-line (format nil "(part_d ~A )" i ))
  (write-line (format nil "============================"))
    (dolist (x i)
        ;(write-line (format nil "~A" x ))
        (write-line (format nil "(part_d ~A ~A)" x (wfp-checkerFOL x)))
      )
  ))

(defun load-start-states (sentence )
  (dolist (i sentence)
  ;(write-line (format nil "(part_b ~A ~A)" i (TruthValue  i)))
  ;(write-line (format nil "(part_d ~A )" i ))
  (write-line (format nil "(part_d ~A ~A)" i (wfp-checkerFOL i)))
  ))

(load-start-states start-state)
(load-start-states goal-state)
(load-start-states operators)
(load-operators operators)


;====================================================================================================

(
 (NOT (P))
 (AND (P)(Q))
 (OR (P)(Q))
 (IMPLIES (P)(Q))
 (EQUIV (P)(Q))
 (EQUIV (IMPLIES (P1) (AND (P2) (Q3))) (NOT (OR (P4) (IMPLIES (P5)(Q6)))))
 (IMPLIES (P)(P))
 (EQUIV (IMPLIES (P)(Q)) (OR (NOT (P))(Q)))
 (EQUIV (NOT (AND (P)(Q))) (OR (NOT (P))(NOT (Q))))
 (IMPLIES (P) (IMPLIES (Q)(P)))
 (OR (P) (NOT (P)))
)
;====================================================================================================

(defun parta-tests ()
  "Unit Tests for part_A"
  ; should pass
  (case? "BOB")
  (case? "B12")
  (case? "P")
  (case? "John is up")

  ; should fail
  (case? "p")
  (case? "B12B")
  (case? "a12")
  (case? "123")
  (case? "John is up")

  ; should fail
  (wfp-checker '(f f f))
  (wfp-checker '(john is up))
  (wfp-checker 'p)
  (wfp-checker '(p q))
  (wfp-checker '(AND (OR P (NOT Q)) (OR (NOT P) Q)))
  (wfp-checker '(NOT P))
  (wfp-checker '(IMPLIES P (Q)))
  (wfp-checker '(IMPLIES (P) Q))
  (wfp-checker '(EQUIV (P) Q))
  (wfp-checker '(EQUIV P (Q)))
  (wfp-checker '(|p|))
  ;Should Pass
  (wfp-checker '(P))
  (wfp-checker '(|P|))
  (wfp-checker '("John is up"))
  (wfp-checker '(NOT (P)))
  (wfp-checker '(IMPLIES (P) (Q)))
  (wfp-checker '(EQUIV (P) (Q)))
  (wfp-checker '(AND (OR (P) (NOT (Q))) (OR (NOT (P)) (Q))))  
  
)


(defun partb-tests ()
  "Unit Tests for part_B"
  ;Should Fail
  (TruthValue '((P t) (Q nil)) '(IMPLIES (P) (Q)))
  (TruthValue '((P t) (Q nil)) '(and (P) (Q)))
  (TruthValue '((P t) (Q nil) (P2 t)) '(and (P) (Q) (P2)))
  (TruthValue '((P t)) '(not (P)))
  (TruthValue '((P nil) (Q nil)) '(or (P) (Q)))


 ;Should Succeed
  (TruthValue '((P t) (Q t)) '(or (P) (Q)))
  (TruthValue '((P t) (Q nil)) '(or (P) (Q)))
  (TruthValue '((P nil) (Q t)) '(or (P) (Q)))
  (TruthValue '((P t) (Q t)) '(and (P) (Q)))
  (TruthValue '((P t) (Q t)) '(IMPLIES (P) (Q)))
  (TruthValue '((P nil)) '((not) (P)))
  (TruthValue '((P t) (Q t)) '(EQUIV (P) (Q)))
  (TruthValue '((P nil) (Q nil)) '(EQUIV (P) (Q)))
  
  
  
  (IsTautology '(OR (P) (NOT (P))))
  (IsTautology '(IMPLIES (P) (Q)))
  (IsTautology '(and (P) (Q)))
  (IsTautology '(EQUIV (P) (Q)))
  (IsTautology '(EQUIV (IMPLIES (P)(Q)) (OR (NOT (P))(Q))))
)



;(part_b (tests expressions) (valuations expressions) )
;(part_b_tautology
;(tests (NOT (P)) (AND (P)(Q)) (OR (P)(Q)) (IMPLIES (P)(Q)) (EQUIV (P)(Q))
;(EQUIV (IMPLIES (P1) (AND (P2) (Q3))) (NOT (OR (P4) (IMPLIES (P5)(Q6)))))
;(IMPLIES (P)(P)) (EQUIV (IMPLIES (P)(Q)) (OR (NOT (P))(Q))) (EQUIV (NOT   
;(AND (P)(Q))) (OR (NOT (P))(NOT (Q)))) (IMPLIES (P) (IMPLIES (Q)(P))) (OR
;(P) (NOT (P)))))
;)

;(part_c ((NOT (P |x| |y| |z|)) (P (|f| |b| |y|) |y|) (IMPLIES (Q |u| (|f| |a| |v|) |d|) (R (|g| (|h| |b| |c| |w|)) |y|)) (ALL |x| (IMPLIES (A |x| |c|) (B |x| |d|))) (ALL |x| (EXISTS |y| (IMPLIES (A |y|) (B |x|)))) (AND (ALL |x| (P |x|)) (Q |y| |z|)) (EQUIV (B |f| |u| |a|) (P ())) (P |x| |a| Q) (ALL |x| |y| (P |x| |y|)) (ALL |x| (IMPLIES (A |y| |c|) (B |x| |d|))) (ALL |z| (EXISTS |y| (IMPLIES (A |y|) (B |x|))))))


;(part_a expression value)
;(part_a (P124) T)

;(part_b expression value)
;(part_b (NOT (P)) T)

;(part_c expression value)
;(part_c (NOT (P |x| |y| |z|)) T)